\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $e$:E, $P$, $R$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. (loc($e$) = $i$) $\Rightarrow$ Dec($R$($e$)))
\\[0ex]$\Rightarrow$ \=(es{-}first{-}at{-}since(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((loc($e$) = $i$)\+
\\[0ex]c$\wedge$ \=($P$($e$) \& ($\neg$$R$($e$))\+
\\[0ex]\& (\=($\exists$${\it e''}$:E. ((${\it e''}$ $<$loc $e$) c$\wedge$ $P$(${\it e''}$)))\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex]((${\it e'}$ $<$loc $e$)
\\[0ex]c$\wedge$ \=($R$(${\it e'}$)\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex](${\it e'}$ $<$loc ${\it e''}$) $\Rightarrow$ (${\it e''}$ $<$loc $e$) $\Rightarrow$ (($\neg$$P$(${\it e''}$)) \& ($\neg$$R$(${\it e''}$)))))))))))
\-\-\-\-\-\-\-
\end{tabbing}